es:ES, P:(E), e:E.
(e':E. e' c e  Dec(P(e')))
 ((e':E. e' c e  (P(e')))
  (m:E. (m c e & P(m) & (x:E. ((m < x) & x c e)  (P(x)))))) 

latex

Definitions	True, T, SQType(T), A c B, False, A, A  B, x:A. B(x), P & Q, , {T}, P  Q, x. t(x), t  T, x(s), P  Q, , x:A. B(x), e c e', Dec(P), SWellFounded(R(x;y))
Lemmas	es-causl wf, max-of-intset, le wf, decidable equal nat, decidable cand, nat wf, not wf, decidable existse-causle, es-causl-swellfnd, event system wf, decidable wf, es-causle wf, es-E wf